\begin{tabbing}
$\forall$$A$,$B$:es\_realizer\{i:l\}.
\\[0ex]($\uparrow$Rplus?($A$))
\\[0ex]$\Rightarrow$ \=($\forall$$i$:Id. \+
\\[0ex]fpf{-}compatible(Knd; $k$.Type; Kind{-}deq; R{-}da(Rplus{-}left($A$); $i$); R{-}da(Rplus{-}right($A$); $i$)))
\-\\[0ex]$\Rightarrow$ \=(R{-}interface($B$; $A$)\+
\\[0ex]$\Leftarrow\!\Rightarrow$ (R{-}interface($B$; Rplus{-}left($A$)) $\wedge$ R{-}interface($B$; Rplus{-}right($A$))))
\-
\end{tabbing}